/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.test.javasyp.logic;

import static com.googlecode.syper.anno.Pred.ensures;
import static com.googlecode.syper.anno.Pred.requires;

import com.googlecode.syper.anno.BoundsChecks;
import com.googlecode.syper.anno.Excl;
import com.googlecode.syper.anno.Imm;
import com.googlecode.syper.anno.Invariant;
import com.googlecode.syper.anno.NullChecks;
import com.googlecode.syper.anno.Old;
import com.googlecode.syper.anno.Pred;
import com.googlecode.syper.anno.Result;
import com.googlecode.syper.anno.ReturnExcl;

import edu.cmu.cs.crystal.annotations.PassingTest;
import edu.cmu.cs.crystal.annotations.UseAnalyses;

/**
 * @author kevin
 * @since May 16, 2010
 */
@NullChecks 
@BoundsChecks
@PassingTest
@UseAnalyses("SymbolicChecker")
public class ArrayList<T> implements Invariant {
	
	@Excl private T[] a;
	private int size;
	
	public ArrayList() {
		this(16);
		ensures(size == 0);
	}

	@SuppressWarnings("unchecked")
	public ArrayList(int initialCapacity) {
		super();
		requires(0 <= initialCapacity);
		a = (T[]) new Object[initialCapacity];
		size = 0;
		ensures(size == 0);
	}
	
	@Imm 
	public T get(int index) {
		imm: {
			requires(0 <= index & index < size);
			return a[index];
		}
	}

	@SuppressWarnings("unchecked")
	@Excl(mod = {"a", "size"})
	public void add(T e) {
		excl: {
			@Old final int oldSize = size;
			@Old final T[] oldA = a;
			if (a.length <= size) {
				@Excl(borrowed = false) T[] newA =
					(T[]) new Object[a.length * 2 + 1];
				for (int i = 0; i < size; ++i) {
					Pred.inv(0 <= i & size == oldSize & oldA == a);
					newA[i] = a[i];
				}
				a = newA;
			}
			a[size++] = e;
			ensures(size == oldSize + 1);
		}
	}

	@Imm 
	public int size() {
		imm: {
			@Result final int result = size;
			ensures(0 <= result & result == size);
			return result;
		}
	}
	
	@ReturnExcl
	@Imm(released = true)
	public ArrIterator<T> iterator() {
		imm: {
			@Result @Excl final ArrIterator<T> result = 
				new ArrIterator<T>(a, size);
			ensures(result != null);
			return result;
		}
	}
	
	@Override
	@Imm
	public boolean inv() {
		imm: return a != null & 0 <= size & size <= a.length;
	}

	public static class ArrIterator<T> implements Invariant {
		
		@Imm private final T[] snapshot;
		private final int count;
		private int index;
		
		public ArrIterator(@Imm(released = true) T[] snapshot, int count) {
			requires(snapshot != null && 0 <= count && count <= snapshot.length);
			this.snapshot = snapshot;
			this.count = count;
			this.index = 0;
		}

		@Imm 
		public boolean hasNext() {
			imm: {
				@Result final boolean result = index < count;
				ensures(result == index < count);
				return result;
			}
		}

		@Excl(mod = "index") 
		public T next() {
			excl: {
				requires(index < count);
				return snapshot[index++];
			}
		}

		@Override
		@Imm
		public boolean inv() {
			imm: return snapshot != null & 0 <= count & count <= snapshot.length & 0 <= index & index <= count;
		}
	}

	public static <T> int hashCode(@Imm ArrayList<T> l) {
		requires(l != null);
		int result = 0;
		for (@Excl ArrIterator<T> it = l.iterator(); it.hasNext(); )
			result += safeHash(it.next());
		return result;
	}
	
	private static int safeHash(Object o) {
		return o == null ? 0 : o.hashCode();
	}

	public static <T> boolean sane(@Imm ArrayList<T> l) {
		requires(l != null);
		@Excl ArrIterator<T> it1 = l.iterator(); 
		@Excl ArrIterator<T> it2 = l.iterator();
		assert it1 != it2;
		while (it1.hasNext() & it2.hasNext()) {
			if (it1.next() != it2.next())
				return false;
		}
		return ! it1.hasNext() & ! it2.hasNext();
	}
	
	@ReturnExcl
	public static <T> ArrayList<T> singleton(T e) {
		@Result @Excl(borrowed = false) final 
		ArrayList<T> result = new ArrayList<T>();
		result.add(e);
		ensures(result.size == 1);
		return result;
	}
}
